Three v1.0 items: E-Grade launcher, mechanized correspondence oracle, RMO secure-deletion runtime#165
Merged
Conversation
Implements the Hyperpolymath E-Grade Launcher Standard (hyperpolymath/standards launcher-standard.adoc/.a2ml) for vsh: - launch.sh: full mode surface --auto/--start/--stop/--status/--browser/ --web/--integ/--disinteg/--help/--version. Version output matches the required 'vsh <version> (<sha>) [<platform>]' format exactly. - Desktop integration (Linux first-class): idempotent --integ/--disinteg, copy-not-symlink launcher, Terminal=true, .desktop at 0444, config+logs preserved on --disinteg. macOS/Windows best-effort. - err()/log(), stderr-always, GUI-error + soft-attach sourced via the published desktop-tools resolution ladder with graceful no-op degradation. - PID/log paths in XDG dirs (never /tmp). - Server-oriented clauses (nohup daemon, wait_for_server URL polling, browser launch) are HONESTLY declared deferred in the a2ml-metadata-block header, since vsh is a foreground terminal shell with no HTTP server. - scripts/run.sh: canonical startup command the standard searches for. - just run / just launch delegate to ./launch.sh --auto. - docs/LAUNCHER.md: conformance attestation + deferred-phase rationale. Verified: --version format, --status, --stop, --auto passthrough, --help, --browser/--web aliases, unknown-mode exit 2, and a full --integ/--disinteg idempotency cycle. shellcheck clean (warning+); bash -n clean. Scope note: full alignment used the public standard fetched from hyperpolymath/standards (that repo is not in this session's GitHub scope). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KfgJznd6jzSeDYsSXGAXkU
Advances the Lean->Rust correspondence toward mechanization by making the compiled proof artifact the test oracle. - proofs/lean4/ModelOracle.lean + lean_exe model_oracle: compiles the exact proven model defs (mkdir/rmdir/createFile/deleteFile/fsUpdate from FilesystemModel + FileOperations) into a standalone executable that reports the node type (DIR/FILE/NONE) at probe paths. - impl/rust-cli/tests/model_oracle_correspondence.rs: generates precondition-respecting op sequences (shadow tracker ensures validity), applies them to the real Rust ShellState, drives the same sequence through the Lean oracle, and asserts model and impl agree at every touched path. 1218 probes agree across 200 sequences. Skips cleanly if the oracle is not built (no Lean toolchain required for ). - just build-model-oracle / test-correspondence-model; wired into lean-verification.yml CI. - docs/LEAN4_RUST_CORRESPONDENCE.md: documents the harness and, honestly, its limits — this is differential testing against the proof artifact, not a full refinement proof (still the v1.0 blocker). Records why the Coq extraction is not executable (Path -> option FSNode function domain + classical axioms in is_empty_dir_dec; needs FMaps.t FSNode migration) and the mechanization roadmap. Verified: lake build model_oracle OK; oracle smoke test matches model semantics (incl. non-recursive rmdir leaving orphan children); differential test passes with and without VSH_MODEL_ORACLE env (auto-detects .lake path). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KfgJznd6jzSeDYsSXGAXkU
…tion)
The obliterate secure-deletion command was fully implemented in
commands/secure_deletion.rs but never wired into dispatch — no Command
variant, no parser case, no executor arm — so it was unreachable dead code
from the REPL/scripts. This binds the proven RMO model to a usable runtime.
Wiring:
- parser: Command::Obliterate { path, force, redirects } + "obliterate" case
(--force/-f skips the confirmation guard).
- executable: executor arm -> commands::secure_deletion::obliterate_path
(routes file vs directory); proof_reference -> OBLITERATE_IRREVERSIBLE;
description arm.
- secure_deletion: obliterate_path dispatcher.
Audit residue (MAA / GDPR Article 17 attestation):
- obliterate/obliterate_dir append an append-only record to
<sandbox-root>/.vsh-audit.log via AuditLog. The data is destroyed; the
proof-of-deletion survives. Sandboxed under the shell root (testable, isolated).
Tests: impl/rust-cli/tests/obliterate_rmo_tests.rs (6) — dispatch wiring,
missing-operand error, end-to-end destruction, audit residue, irreversibility
(undo cannot resurrect), no-old-plaintext-remains. Full suite green (317 lib +
all integration); verified through the real vsh binary in script mode.
Honest scope (docs reconciled from "RMO stubs only"): best-effort 3-pass
overwrite (random/0x00/0xFF + fsync) on in-place filesystems only; CoW/SSD need
hardware secure_erase; audit HMAC signing pending; NOT a complete GDPR
framework. Updated CLAUDE.md, README, FAQ, ROADMAP(+_TO_V1), TOPOLOGY,
docs/wiki/*, methodology.a2ml, and the ECHO-TYPES-OCHRANCE bridge (adoc + a2ml)
in lock-step.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01KfgJznd6jzSeDYsSXGAXkU
🔍 Hypatia Security ScanFindings: 41 issues detected
View findings[
{
"reason": "Agda postulate assumes without proof -- potential soundness hole (1 occurrences, CWE-704)",
"type": "agda_postulate",
"file": "/home/runner/work/valence-shell/valence-shell/proofs/agda/FilesystemModel.agda",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "believe_me undermines formal verification (2 occurrences, CWE-704)",
"type": "believe_me",
"file": "/home/runner/work/valence-shell/valence-shell/proofs/idris2/src/Filesystem/Axioms.idr",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "Obj.magic bypassing type safety (2 occurrences, CWE-704)",
"type": "obj_magic",
"file": "/home/runner/work/valence-shell/valence-shell/impl/mcp/src/bindings/Mcp.res",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "JSON decode without validation (1 occurrences, CWE-20)",
"type": "json_decode_no_validation",
"file": "/home/runner/work/valence-shell/valence-shell/impl/mcp/src/Server.res",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "expect() in hot path (1 occurrences, CWE-754)",
"type": "expect_in_hot_path",
"file": "/home/runner/work/valence-shell/valence-shell/impl/rust-cli/src/external.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "unsafe block -- requires SAFETY comment (6 occurrences, CWE-676)",
"type": "unsafe_block",
"file": "/home/runner/work/valence-shell/valence-shell/impl/rust-cli/src/external.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "from_raw constructs types from raw pointers without safety checks (4 occurrences, CWE-676)",
"type": "from_raw",
"file": "/home/runner/work/valence-shell/valence-shell/impl/rust-cli/src/external.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "expect() in hot path (1 occurrences, CWE-754)",
"type": "expect_in_hot_path",
"file": "/home/runner/work/valence-shell/valence-shell/impl/rust-cli/src/glob.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "expect() in hot path (1 occurrences, CWE-754)",
"type": "expect_in_hot_path",
"file": "/home/runner/work/valence-shell/valence-shell/impl/rust-cli/src/arith.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "unsafe block -- requires SAFETY comment (2 occurrences, CWE-676)",
"type": "unsafe_block",
"file": "/home/runner/work/valence-shell/valence-shell/impl/rust-cli/src/process_sub.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
CI (Rust 1.97) failed two checks on this branch:
- rustfmt: new test files + the Obliterate executor arm needed formatting.
- clippy -D warnings: unneeded_wildcard_pattern (field: _ redundant with ..)
in commands.rs (Chmod/Chown) and parser.rs (External/Touch), which clippy
1.97 newly errors on; plus a pre-existing let_and_return in the ${VAR:=default}
expansion path.
Fixes:
- cargo fmt across the crate (new tests + executable.rs).
- Remove redundant bindings where already covers them.
- Inline the let-and-return in AssignDefault expansion (behavior unchanged).
Verified against CI's exact toolchain: cargo +1.97.0 clippy --all-targets
--all-features -- -D warnings is clean; cargo +1.97.0 fmt --check has 0 diffs.
Full lib suite (317) + obliterate RMO tests (6) still green.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01KfgJznd6jzSeDYsSXGAXkU
🔍 Hypatia Security ScanFindings: 41 issues detected
View findings[
{
"reason": "Agda postulate assumes without proof -- potential soundness hole (1 occurrences, CWE-704)",
"type": "agda_postulate",
"file": "/home/runner/work/valence-shell/valence-shell/proofs/agda/FilesystemModel.agda",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "believe_me undermines formal verification (2 occurrences, CWE-704)",
"type": "believe_me",
"file": "/home/runner/work/valence-shell/valence-shell/proofs/idris2/src/Filesystem/Axioms.idr",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "Obj.magic bypassing type safety (2 occurrences, CWE-704)",
"type": "obj_magic",
"file": "/home/runner/work/valence-shell/valence-shell/impl/mcp/src/bindings/Mcp.res",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "JSON decode without validation (1 occurrences, CWE-20)",
"type": "json_decode_no_validation",
"file": "/home/runner/work/valence-shell/valence-shell/impl/mcp/src/Server.res",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "expect() in hot path (1 occurrences, CWE-754)",
"type": "expect_in_hot_path",
"file": "/home/runner/work/valence-shell/valence-shell/impl/rust-cli/src/external.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "unsafe block -- requires SAFETY comment (6 occurrences, CWE-676)",
"type": "unsafe_block",
"file": "/home/runner/work/valence-shell/valence-shell/impl/rust-cli/src/external.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "from_raw constructs types from raw pointers without safety checks (4 occurrences, CWE-676)",
"type": "from_raw",
"file": "/home/runner/work/valence-shell/valence-shell/impl/rust-cli/src/external.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "expect() in hot path (1 occurrences, CWE-754)",
"type": "expect_in_hot_path",
"file": "/home/runner/work/valence-shell/valence-shell/impl/rust-cli/src/glob.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "expect() in hot path (1 occurrences, CWE-754)",
"type": "expect_in_hot_path",
"file": "/home/runner/work/valence-shell/valence-shell/impl/rust-cli/src/arith.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "unsafe block -- requires SAFETY comment (2 occurrences, CWE-676)",
"type": "unsafe_block",
"file": "/home/runner/work/valence-shell/valence-shell/impl/rust-cli/src/process_sub.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
hyperpolymath
marked this pull request as ready for review
July 17, 2026 06:10
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Three outstanding items, in order, each verified with the real toolchain.
1 — Launcher conforms to the E-Grade Launcher Standard
launch.shimplements the Hyperpolymath E-Grade Launcher Standard (fetched from the publichyperpolymath/standards): full mode surface--auto/--start/--stop/--status/--browser/--web/--integ/--disinteg/--help/--version, version formatvsh <ver> (<sha>) [<platform>], idempotent Linux desktop integration (copy-not-symlink,Terminal=true,.desktopat 0444, config/logs preserved on--disinteg), desktop-tools resolution ladder with graceful no-op degradation, XDG PID/log paths.Because
vshis a foreground terminal shell with no server, the server-oriented clauses (nohup daemon,wait_for_serverURL polling, browser launch) are honestly declared deferred in thea2ml-metadata-blockheader rather than silently skipped.scripts/run.shis the canonical startup command the standard searches for;just run/just launchdelegate to it.docs/LAUNCHER.mdis the conformance attestation.Verified: every mode, a full
--integ/--disintegidempotency cycle, shellcheck clean.2 — Mechanized correspondence: compiled proven model as test oracle
proofs/lean4/ModelOracle.lean(lean_exe model_oracle) compiles the exact proven model defs (mkdir/rmdir/createFile/deleteFile/fsUpdate) into an oracle.impl/rust-cli/tests/model_oracle_correspondence.rsgenerates precondition-respecting sequences, applies them to the real RustShellState, drives the same sequence through the compiled Lean model, and asserts agreement at every touched path.1218 probes agree across 200 sequences. This makes the proof artifact itself the oracle (stronger than hand-transcribed property tests) — but it is honestly still differential testing, not a full refinement proof (the v1.0 blocker).
docs/LEAN4_RUST_CORRESPONDENCE.mddocuments why the Coq extraction is not executable (Path → option FSNodedomain + classical axioms inis_empty_dir_dec; needsFMaps.t FSNodemigration) and the roadmap. Wired intolean-verification.ymlCI;just test-correspondence-model.3 — RMO secure-deletion runtime (the big one)
obliteratewas fully implemented incommands/secure_deletion.rsbut never wired into dispatch — unreachable dead code. Added theCommand::Obliteratevariant, parser case (--force), and executor arm →secure_deletion::obliterate_path. Added the audit residue: obliterate appends to<sandbox-root>/.vsh-audit.log— the MAA/GDPR-Art.17 attestation that survives the deletion.Verified:
impl/rust-cli/tests/obliterate_rmo_tests.rs(6 tests — wiring, destruction, audit residue, irreversibility, no-plaintext-remains), full suite green, and driven through the realvshbinary in script mode.Honest scope: best-effort 3-pass overwrite on in-place filesystems only; CoW/SSD need hardware
secure_erase; audit HMAC signing pending; not a complete GDPR framework. Status docs reconciled from "RMO stubs only" across CLAUDE.md, README, FAQ, ROADMAP(+_TO_V1), TOPOLOGY,docs/wiki/*,methodology.a2ml, and the ECHO-TYPES-OCHRANCE bridge (adoc + a2ml, in lock-step).What remains genuinely open
Full mechanized Lean→Rust refinement proof and a complete GDPR/RMO framework (hardware erase, HMAC-signed audit) — both flagged honestly in-repo, neither overclaimed.
🤖 Generated with Claude Code
https://claude.ai/code/session_01KfgJznd6jzSeDYsSXGAXkU
Generated by Claude Code